f(0, 1, x) → f(g(x), g(x), x)
f(g(x), y, z) → g(f(x, y, z))
f(x, g(y), z) → g(f(x, y, z))
f(x, y, g(z)) → g(f(x, y, z))
↳ QTRS
↳ DependencyPairsProof
f(0, 1, x) → f(g(x), g(x), x)
f(g(x), y, z) → g(f(x, y, z))
f(x, g(y), z) → g(f(x, y, z))
f(x, y, g(z)) → g(f(x, y, z))
F(0, 1, x) → F(g(x), g(x), x)
F(x, g(y), z) → F(x, y, z)
F(g(x), y, z) → F(x, y, z)
F(x, y, g(z)) → F(x, y, z)
f(0, 1, x) → f(g(x), g(x), x)
f(g(x), y, z) → g(f(x, y, z))
f(x, g(y), z) → g(f(x, y, z))
f(x, y, g(z)) → g(f(x, y, z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
F(0, 1, x) → F(g(x), g(x), x)
F(x, g(y), z) → F(x, y, z)
F(g(x), y, z) → F(x, y, z)
F(x, y, g(z)) → F(x, y, z)
f(0, 1, x) → f(g(x), g(x), x)
f(g(x), y, z) → g(f(x, y, z))
f(x, g(y), z) → g(f(x, y, z))
f(x, y, g(z)) → g(f(x, y, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(x, y, g(z)) → F(x, y, z)
Used ordering: Polynomial interpretation [25,35]:
F(0, 1, x) → F(g(x), g(x), x)
F(x, g(y), z) → F(x, y, z)
F(g(x), y, z) → F(x, y, z)
The value of delta used in the strict ordering is 1/16.
POL(g(x1)) = 1/4 + x_1
POL(F(x1, x2, x3)) = (1/4)x_3
POL(0) = 0
POL(1) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
F(0, 1, x) → F(g(x), g(x), x)
F(x, g(y), z) → F(x, y, z)
F(g(x), y, z) → F(x, y, z)
f(0, 1, x) → f(g(x), g(x), x)
f(g(x), y, z) → g(f(x, y, z))
f(x, g(y), z) → g(f(x, y, z))
f(x, y, g(z)) → g(f(x, y, z))